Inference at * 2 2 2 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. 0 < ||L1||
7. 0 < ||L2||
8. x = last(L1)
9. y = hd(L2)
  y = L2[(((||L1|| - 1)+1) - ||L1||)] 

latex

 by ((DVar `L2') 
CollapseTHEN (((All Reduce) 
CollapseTHEN (Auto')))) 

latex

C1: 

C1: 5. u : T
C1: 6. v : T List
C1: 7. 0 < ||L1||
C1: 8. 0 < (||v||+1)
C1: 9. x = last(L1)
C1: 10. y = u
C1:   y = [u / v][(((||L1|| - 1)+1) - ||L1||)]
C.

Definitions

[], hd(l), l[i], n+m, n - m, #$n, [car / cdr], last(L), a < b, type List, Type, s = t, ||as||, i  j